Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

Herzlich willkommen. Sie sehen hier doch auch ich habe einen Computer.

Wir wollen uns jetzt noch mal kurz die Geschichte mit diesen Beweisassistenten ansehen.

Der ist in den Übungen ja dran gewesen und Herr Goncharow hat mir berichtet, dass Sie sich damit noch nicht so ganz anfreunden können oder vielleicht nicht so interessiert dran sind oder was auch immer.

Das heißt, ich mache jetzt noch mal eine kurze Demo. Die hat nicht das Ziel, Ihnen das Tool komplett zu erklären.

Das Tool ist sehr gut erklärt, zum Beispiel in diesem Cheatsheet von Andre Bauer, dass das auf den Homepages verlinkt ist.

Und sonst geht man damit um, wie halt mit jedem Tool, wie Sie auch mit dem GCC umgehen usw.

Sie lesen sich halt die Dokumentation durch oder Sie probieren das mal.

Das Tool selbst ist natürlich nicht direkt klausurrelevant. Wie soll ich das machen?

Im Gegenteil, lasse ich zwei Hilfsmittel, zuschließe dabei aber Laptops ausdrücklich aus und das wäre natürlich nicht mehr möglich, wenn ich irgendwie Aufgaben auf Koks stelle.

Der Zweck der Verwendung dieses Tools ist, dass Sie ein Gefühl dafür kriegen, wie man korrekt solche formalen Beweise baut.

Und das ist sicher relevant am Ende für die Klausur, wie man solche Beweise baut.

Wir haben eine Weile gesucht, dass das Tool nicht ganz eins zu eins diesen Fitch-Kalkül nachmodelliert, aber im Wesentlichen.

Herr Goncharow hat online eine Übersetzung zwischen Regeln des Fitch-Kalküls und Taktiken in diesem Tool gestellt.

Die ist so ein bisschen cum granosales zu nehmen. Es ist jetzt nicht so, dass man das per Copy-Paste hier reinsetzen könnte, den Text, den er da verfasst hat, und dann jedes Mal genau die Wirkung der Regel bekommt.

Aber es ist wirklich von den Taktiken her ziemlich nah dran an den Regeln, die man im Fitch-Kalkül verwendet.

Das heißt, wenn Sie das hier können, dann kriegen Sie Fitch auch hin.

Ich werde das jetzt einmal, um Ihr Interesse daran zu wecken, soweit Sie es eben in den Übungen noch nicht gesehen haben.

Die Übungen sind natürlich, die Abgabe der Übung ist ja nicht verpflichtend, insofern kennen das vielleicht viele nicht.

Ich werde das einfach mal demonstrieren.

Also, ja gut, es gibt so einen Header, den können Sie vergessen. Das importieren Sie einfach immer.

Und wir stellen jetzt hier eine Behauptung auf, die da vorne Parameter hat. Das ist so ein bisschen, als würde man in einem von Hand aufgeschriebenen Theorem sagen, für alle PQR gilt.

Das ist nur, um jetzt also im Theorem diesen expliziten Quantor zu vermeiden, sagt man stattdessen Parameter.

Das hat man PQR im Beweis dann gleich fest in der Hand. Gut, und ja, was das Theorem sagt, das ist im Grunde so eine Achilles- und die Schildkröte-mäßige Kollabierung der Disjunktions-Eliminationsregel.

Das besagt mir also praktisch, dass ich, wenn ich zwei Implikationen habe, wo beide Male Q impliziert wird, einmal von P und einmal von R, dass Q dann auch von P oder R impliziert wird.

Ja, wenn Sie sich erinnern, wie die Disjunktions-Eliminationsregel aussieht, die sieht praktisch genauso aus, nur dass da die Implikationspfeile, naja, soweit sie vor dem äußersten Implikationspfeil stehen, sind das Unterbeweise statt Implikationen.

Und der oberste, also dieser hier, das ist schlicht und auffert der Regelstrich. So, ich sag jetzt mal wieder hier, nächstes Kommando vorwärts, das wird also dann jetzt das Theorem verarbeiten.

Das ist ein kleines, verarbeitet Parameter, okay. So, jetzt haben wir hier in dem rechten Fenster da ein Beweisziel, naja, nämlich das, was wir gerade als Theorem behauptet haben, das müssen wir jetzt also beweisen.

Und wir beginnen dazu einen Beweis, wie wir das auf Papier auch machen würden, wir sagen Proof. So, da ändert sich zunächst mal noch nichts mit.

So, und jetzt verwenden wir Regel. Und wir machen das tatsächlich, ja, wie gesagt, fast eins zu eins, so wie wir das jetzt in Fitch auch machen würden.

Was sehen wir hier ganz oben? Wir sehen ganz oben, Laser-Point habe ich nicht, aber es gibt, ho, Wahnsinn.

Also, es gibt hier oben, ja, als oberstes Konnektiv ein Implikationszeichen. Das ganz oben liegt daran, dass erstens das Ding hier rechts assoziativ bindet, das heißt, hier ist so rum geklammert, und zweitens und bindet stärker, das heißt, hier ist auch eine Klammer, das wir also beides nicht sehen.

Also, das oberste Konnektiv ist dieses hier. Wenn wir das beweisen wollen, müssen wir also eine Implikationseinführung machen. So, er hat jetzt für solche Einführungsregeln eine Taktik, wo er dann einfach die passende Einführungsregel anwendet, das ist also schon so ein bisschen Intelligenz, die da eingebaut ist, nicht viel Intelligenz, aber immerhin.

So, ich sage also Intro. Was er macht, ist also die korrekte Einführungsregel anwenden, das heißt, er gibt mir hier folgende Beweisaufgabe, ich muss annehmen, was vor dem Implikationszeichen stand, das ist das hier, und ich muss beweisen, was dahinter stand, das ist das hier.

So, nun sehen wir als aktuelles Beweisziel wieder eine Implikation, das heißt, wir gehen reflexartig weiter per Implikationseinführung, das heißt, hier in Coq wieder per Intro, also, Nächster.

So, das heißt, wir haben jetzt eine zusätzliche Annahme, das, was vorher vor dem Implikationszeichen stand, also P oder R, und wir müssen beweisen Q.

So, jetzt sind wir hier in der Situation, dass wir dieses P oder R ausnutzen müssen. Das müssen wir nutzen und haben also dann praktisch zwei Fälle, entweder P gilt, dann können wir diese Implikation verwenden, oder R gilt, dann können wir diese Implikation verwenden.

So, das ist genau die Dysjunktionseliminationsregel, klar, dass die dahinter steckt, denn unser Beweisziel war ja praktisch diese Regel nur eben als Formel. So, und dazu liefert Coq jetzt diese Taktik hier, destruct.

Destruct ist praktisch die Dysjunktionseliminationsregel. Wenn ich das jetzt anwende, dann gebe ich dir mein Argument mit H, das ist also hier oben diese Hypothese hier, die Annahme, das ist also das, was, ah nee, andersrum.

Es ist wahrscheinlich egal, in welcher Reihenfolge ich das machen, ich versuche das mal zu vertauschen auf das Risiko hin, dass das gleich schief geht, aber es müsste eigentlich gehen.

Das ist wieder der Nachteil. So, wir vertauschen das. So, also, hier das H0, darauf wende ich jetzt die Dysjunktionseliminationsregel an, dann bekomme ich zwei Unterbeweise, die jeweils, also irgendwie ist das ja doch nicht so ganz praktisch.

Dann bekomme ich so ganz praktisch mit diesem Ding, wir legen das mal hier hin. So, dann bekomme ich zwei Unterbeweise, einen, in dem ich als Annahme P habe und einen, in dem ich als Annahme R habe.

So, und dieses L oder R, wie sich das hier liest, das vergibt also einfach nur Namen für diese Annahmen, die ich dann in diesen Unterbeweisen bekomme.

Ich sehe merkwürdigerweise nur einen Unterbeweis, das liegt daran, dass halt Coq den anderen erstmal versteckt und mir immer nur einen zur Zeit präsentiert.

Wir werden sehen, dass der andere Teilbeweis, den ich noch erledigen muss, auftauche, sobald dieser hier erledigt ist.

So, jetzt habe ich, ja, wie muss ich das jetzt machen? Wenn ich jetzt hier meine Annahme P habe und Q zeigen will, dann muss ich diesen Teil hier von H verwenden, an den ich rankomme, in dem ich Konjunktionselimination mache.

Also auf der linken Seite, da kann ich ja P impliziert Q folgern. So, wiederum wird also Konjunktionselimination, wie die andere Eliminationsregel auch, als eine Destruct-Taktik implementiert, die diesmal leicht andere Syntax hat, da fehlt halt dieses oder.

Ansonsten ist das genau das selbe. So, das heißt, wenn ich jetzt Destruct auf H anwende, dann bekomme ich zwei Dinge, die daraus folgen und die kriegen Namen, die ich hier vornehme, H1 und H2.

So, ich mache das mal. So, jetzt habe ich hier H1, das ist der linke Teil, H2, der rechte Teil. Ich kann auch zum Beispiel bei einem Unterstrich machen, wenn er mich nicht interessiert, dann kriege ich keinen Namen.

So, jetzt kann ich also hier dieses H1, P impliziert Q, da kann ich Implikationselimination machen, zusammen mit dem P, also dem L, hier Annahme L.